YES 1.618 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



HASKELL
  ↳ BR

mainModule Main
  (((==) :: Eq a => Maybe a  ->  Maybe a  ->  Bool) :: Eq a => Maybe a  ->  Maybe a  ->  Bool)

module Main where
  import qualified Prelude



Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL
  ↳ BR
HASKELL
      ↳ COR

mainModule Main
  (((==) :: Eq a => Maybe a  ->  Maybe a  ->  Bool) :: Eq a => Maybe a  ->  Maybe a  ->  Bool)

module Main where
  import qualified Prelude



Cond Reductions:
The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
HASKELL
          ↳ Narrow

mainModule Main
  ((==) :: Eq a => Maybe a  ->  Maybe a  ->  Bool)

module Main where
  import qualified Prelude



Haskell To QDPs


↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat(Succ(xv1100), Succ(xv401000)) → new_primPlusNat(xv1100, xv401000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMulNat(Succ(xv30100), Succ(xv40100)) → new_primMulNat(xv30100, Succ(xv40100))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primEqNat(Succ(xv3000), Succ(xv4000)) → new_primEqNat(xv3000, xv4000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_esEs1(Just(@2(xv300, xv301)), Just(@2(xv400, xv401)), app(app(ty_@2, app(ty_[], bah)), bba)) → new_esEs(xv300, xv400, bah)
new_esEs1(Just(@3(xv300, xv301, xv302)), Just(@3(xv400, xv401, xv402)), app(app(app(ty_@3, app(ty_Maybe, db)), cd), ce)) → new_esEs1(xv300, xv400, db)
new_esEs2(Right(xv300), Right(xv400), hf, app(ty_[], hg)) → new_esEs(xv300, xv400, hg)
new_esEs2(Left(xv300), Left(xv400), app(app(ty_@2, hd), he), ge) → new_esEs3(xv300, xv400, hd, he)
new_esEs1(Just(:(xv300, xv301)), Just(:(xv400, xv401)), app(ty_[], app(app(ty_@2, bh), ca))) → new_esEs3(xv300, xv400, bh, ca)
new_esEs0(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), app(app(ty_Either, dc), dd), cd, ce) → new_esEs2(xv300, xv400, dc, dd)
new_esEs1(Just(Left(xv300)), Just(Left(xv400)), app(app(ty_Either, app(app(ty_Either, hb), hc)), ge)) → new_esEs2(xv300, xv400, hb, hc)
new_esEs1(Just(@3(xv300, xv301, xv302)), Just(@3(xv400, xv401, xv402)), app(app(app(ty_@3, dg), app(ty_[], dh)), ce)) → new_esEs(xv301, xv401, dh)
new_esEs3(@2(xv300, xv301), @2(xv400, xv401), app(ty_[], bah), bba) → new_esEs(xv300, xv400, bah)
new_esEs3(@2(xv300, xv301), @2(xv400, xv401), app(app(app(ty_@3, bbb), bbc), bbd), bba) → new_esEs0(xv300, xv400, bbb, bbc, bbd)
new_esEs1(Just(:(xv300, xv301)), Just(:(xv400, xv401)), app(ty_[], app(ty_[], ba))) → new_esEs(xv300, xv400, ba)
new_esEs2(Left(xv300), Left(xv400), app(app(ty_Either, hb), hc), ge) → new_esEs2(xv300, xv400, hb, hc)
new_esEs0(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), dg, cd, app(ty_[], fa)) → new_esEs(xv302, xv402, fa)
new_esEs1(Just(@2(xv300, xv301)), Just(@2(xv400, xv401)), app(app(ty_@2, bcb), app(app(ty_@2, bdb), bdc))) → new_esEs3(xv301, xv401, bdb, bdc)
new_esEs2(Left(xv300), Left(xv400), app(ty_Maybe, ha), ge) → new_esEs1(xv300, xv400, ha)
new_esEs1(Just(@3(xv300, xv301, xv302)), Just(@3(xv400, xv401, xv402)), app(app(app(ty_@3, dg), app(app(app(ty_@3, ea), eb), ec)), ce)) → new_esEs0(xv301, xv401, ea, eb, ec)
new_esEs3(@2(xv300, xv301), @2(xv400, xv401), bcb, app(ty_[], bcc)) → new_esEs(xv301, xv401, bcc)
new_esEs1(Just(@3(xv300, xv301, xv302)), Just(@3(xv400, xv401, xv402)), app(app(app(ty_@3, dg), cd), app(app(ty_@2, ga), gb))) → new_esEs3(xv302, xv402, ga, gb)
new_esEs0(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), app(app(ty_@2, de), df), cd, ce) → new_esEs3(xv300, xv400, de, df)
new_esEs3(@2(xv300, xv301), @2(xv400, xv401), bcb, app(ty_Maybe, bcg)) → new_esEs1(xv301, xv401, bcg)
new_esEs1(Just(@3(xv300, xv301, xv302)), Just(@3(xv400, xv401, xv402)), app(app(app(ty_@3, dg), app(app(ty_@2, eg), eh)), ce)) → new_esEs3(xv301, xv401, eg, eh)
new_esEs1(Just(Right(xv300)), Just(Right(xv400)), app(app(ty_Either, hf), app(ty_Maybe, bac))) → new_esEs1(xv300, xv400, bac)
new_esEs1(Just(@2(xv300, xv301)), Just(@2(xv400, xv401)), app(app(ty_@2, bcb), app(ty_[], bcc))) → new_esEs(xv301, xv401, bcc)
new_esEs0(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), dg, app(ty_[], dh), ce) → new_esEs(xv301, xv401, dh)
new_esEs1(Just(Right(xv300)), Just(Right(xv400)), app(app(ty_Either, hf), app(app(ty_Either, bad), bae))) → new_esEs2(xv300, xv400, bad, bae)
new_esEs1(Just(Left(xv300)), Just(Left(xv400)), app(app(ty_Either, app(ty_[], gd)), ge)) → new_esEs(xv300, xv400, gd)
new_esEs2(Right(xv300), Right(xv400), hf, app(app(ty_Either, bad), bae)) → new_esEs2(xv300, xv400, bad, bae)
new_esEs3(@2(xv300, xv301), @2(xv400, xv401), app(app(ty_@2, bbh), bca), bba) → new_esEs3(xv300, xv400, bbh, bca)
new_esEs1(Just(@3(xv300, xv301, xv302)), Just(@3(xv400, xv401, xv402)), app(app(app(ty_@3, app(ty_[], cc)), cd), ce)) → new_esEs(xv300, xv400, cc)
new_esEs1(Just(xv30), Just(xv40), app(ty_Maybe, gc)) → new_esEs1(xv30, xv40, gc)
new_esEs3(@2(xv300, xv301), @2(xv400, xv401), bcb, app(app(app(ty_@3, bcd), bce), bcf)) → new_esEs0(xv301, xv401, bcd, bce, bcf)
new_esEs0(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), dg, cd, app(app(ty_Either, fg), fh)) → new_esEs2(xv302, xv402, fg, fh)
new_esEs3(@2(xv300, xv301), @2(xv400, xv401), bcb, app(app(ty_Either, bch), bda)) → new_esEs2(xv301, xv401, bch, bda)
new_esEs3(@2(xv300, xv301), @2(xv400, xv401), app(app(ty_Either, bbf), bbg), bba) → new_esEs2(xv300, xv400, bbf, bbg)
new_esEs1(Just(@2(xv300, xv301)), Just(@2(xv400, xv401)), app(app(ty_@2, app(app(ty_Either, bbf), bbg)), bba)) → new_esEs2(xv300, xv400, bbf, bbg)
new_esEs1(Just(@3(xv300, xv301, xv302)), Just(@3(xv400, xv401, xv402)), app(app(app(ty_@3, app(app(ty_Either, dc), dd)), cd), ce)) → new_esEs2(xv300, xv400, dc, dd)
new_esEs1(Just(:(xv300, xv301)), Just(:(xv400, xv401)), app(ty_[], app(ty_Maybe, be))) → new_esEs1(xv300, xv400, be)
new_esEs2(Left(xv300), Left(xv400), app(app(app(ty_@3, gf), gg), gh), ge) → new_esEs0(xv300, xv400, gf, gg, gh)
new_esEs1(Just(:(xv300, xv301)), Just(:(xv400, xv401)), app(ty_[], app(app(app(ty_@3, bb), bc), bd))) → new_esEs0(xv300, xv400, bb, bc, bd)
new_esEs1(Just(Left(xv300)), Just(Left(xv400)), app(app(ty_Either, app(ty_Maybe, ha)), ge)) → new_esEs1(xv300, xv400, ha)
new_esEs1(Just(Left(xv300)), Just(Left(xv400)), app(app(ty_Either, app(app(ty_@2, hd), he)), ge)) → new_esEs3(xv300, xv400, hd, he)
new_esEs2(Left(xv300), Left(xv400), app(ty_[], gd), ge) → new_esEs(xv300, xv400, gd)
new_esEs1(Just(@3(xv300, xv301, xv302)), Just(@3(xv400, xv401, xv402)), app(app(app(ty_@3, dg), cd), app(app(app(ty_@3, fb), fc), fd))) → new_esEs0(xv302, xv402, fb, fc, fd)
new_esEs1(Just(@2(xv300, xv301)), Just(@2(xv400, xv401)), app(app(ty_@2, bcb), app(app(app(ty_@3, bcd), bce), bcf))) → new_esEs0(xv301, xv401, bcd, bce, bcf)
new_esEs0(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), dg, app(ty_Maybe, ed), ce) → new_esEs1(xv301, xv401, ed)
new_esEs1(Just(@3(xv300, xv301, xv302)), Just(@3(xv400, xv401, xv402)), app(app(app(ty_@3, dg), app(app(ty_Either, ee), ef)), ce)) → new_esEs2(xv301, xv401, ee, ef)
new_esEs0(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), dg, cd, app(app(ty_@2, ga), gb)) → new_esEs3(xv302, xv402, ga, gb)
new_esEs1(Just(Left(xv300)), Just(Left(xv400)), app(app(ty_Either, app(app(app(ty_@3, gf), gg), gh)), ge)) → new_esEs0(xv300, xv400, gf, gg, gh)
new_esEs1(Just(:(xv300, xv301)), Just(:(xv400, xv401)), app(ty_[], app(app(ty_Either, bf), bg))) → new_esEs2(xv300, xv400, bf, bg)
new_esEs1(Just(@2(xv300, xv301)), Just(@2(xv400, xv401)), app(app(ty_@2, app(app(ty_@2, bbh), bca)), bba)) → new_esEs3(xv300, xv400, bbh, bca)
new_esEs1(Just(@3(xv300, xv301, xv302)), Just(@3(xv400, xv401, xv402)), app(app(app(ty_@3, dg), cd), app(ty_[], fa))) → new_esEs(xv302, xv402, fa)
new_esEs2(Right(xv300), Right(xv400), hf, app(app(app(ty_@3, hh), baa), bab)) → new_esEs0(xv300, xv400, hh, baa, bab)
new_esEs1(Just(:(xv300, xv301)), Just(:(xv400, xv401)), app(ty_[], cb)) → new_esEs(xv301, xv401, cb)
new_esEs1(Just(@2(xv300, xv301)), Just(@2(xv400, xv401)), app(app(ty_@2, bcb), app(app(ty_Either, bch), bda))) → new_esEs2(xv301, xv401, bch, bda)
new_esEs3(@2(xv300, xv301), @2(xv400, xv401), app(ty_Maybe, bbe), bba) → new_esEs1(xv300, xv400, bbe)
new_esEs0(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), dg, app(app(app(ty_@3, ea), eb), ec), ce) → new_esEs0(xv301, xv401, ea, eb, ec)
new_esEs2(Right(xv300), Right(xv400), hf, app(app(ty_@2, baf), bag)) → new_esEs3(xv300, xv400, baf, bag)
new_esEs1(Just(Right(xv300)), Just(Right(xv400)), app(app(ty_Either, hf), app(app(ty_@2, baf), bag))) → new_esEs3(xv300, xv400, baf, bag)
new_esEs1(Just(@2(xv300, xv301)), Just(@2(xv400, xv401)), app(app(ty_@2, app(app(app(ty_@3, bbb), bbc), bbd)), bba)) → new_esEs0(xv300, xv400, bbb, bbc, bbd)
new_esEs0(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), dg, app(app(ty_@2, eg), eh), ce) → new_esEs3(xv301, xv401, eg, eh)
new_esEs1(Just(@2(xv300, xv301)), Just(@2(xv400, xv401)), app(app(ty_@2, bcb), app(ty_Maybe, bcg))) → new_esEs1(xv301, xv401, bcg)
new_esEs1(Just(Right(xv300)), Just(Right(xv400)), app(app(ty_Either, hf), app(app(app(ty_@3, hh), baa), bab))) → new_esEs0(xv300, xv400, hh, baa, bab)
new_esEs3(@2(xv300, xv301), @2(xv400, xv401), bcb, app(app(ty_@2, bdb), bdc)) → new_esEs3(xv301, xv401, bdb, bdc)
new_esEs1(Just(@3(xv300, xv301, xv302)), Just(@3(xv400, xv401, xv402)), app(app(app(ty_@3, dg), app(ty_Maybe, ed)), ce)) → new_esEs1(xv301, xv401, ed)
new_esEs0(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), app(ty_[], cc), cd, ce) → new_esEs(xv300, xv400, cc)
new_esEs(:(xv300, xv301), :(xv400, xv401), cb) → new_esEs(xv301, xv401, cb)
new_esEs1(Just(@3(xv300, xv301, xv302)), Just(@3(xv400, xv401, xv402)), app(app(app(ty_@3, app(app(app(ty_@3, cf), cg), da)), cd), ce)) → new_esEs0(xv300, xv400, cf, cg, da)
new_esEs0(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), dg, cd, app(app(app(ty_@3, fb), fc), fd)) → new_esEs0(xv302, xv402, fb, fc, fd)
new_esEs0(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), dg, cd, app(ty_Maybe, ff)) → new_esEs1(xv302, xv402, ff)
new_esEs(:(xv300, xv301), :(xv400, xv401), app(app(ty_Either, bf), bg)) → new_esEs2(xv300, xv400, bf, bg)
new_esEs1(Just(@3(xv300, xv301, xv302)), Just(@3(xv400, xv401, xv402)), app(app(app(ty_@3, dg), cd), app(app(ty_Either, fg), fh))) → new_esEs2(xv302, xv402, fg, fh)
new_esEs(:(xv300, xv301), :(xv400, xv401), app(app(app(ty_@3, bb), bc), bd)) → new_esEs0(xv300, xv400, bb, bc, bd)
new_esEs2(Right(xv300), Right(xv400), hf, app(ty_Maybe, bac)) → new_esEs1(xv300, xv400, bac)
new_esEs1(Just(@3(xv300, xv301, xv302)), Just(@3(xv400, xv401, xv402)), app(app(app(ty_@3, dg), cd), app(ty_Maybe, ff))) → new_esEs1(xv302, xv402, ff)
new_esEs1(Just(@3(xv300, xv301, xv302)), Just(@3(xv400, xv401, xv402)), app(app(app(ty_@3, app(app(ty_@2, de), df)), cd), ce)) → new_esEs3(xv300, xv400, de, df)
new_esEs(:(xv300, xv301), :(xv400, xv401), app(app(ty_@2, bh), ca)) → new_esEs3(xv300, xv400, bh, ca)
new_esEs0(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), app(ty_Maybe, db), cd, ce) → new_esEs1(xv300, xv400, db)
new_esEs1(Just(Right(xv300)), Just(Right(xv400)), app(app(ty_Either, hf), app(ty_[], hg))) → new_esEs(xv300, xv400, hg)
new_esEs0(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), dg, app(app(ty_Either, ee), ef), ce) → new_esEs2(xv301, xv401, ee, ef)
new_esEs1(Just(@2(xv300, xv301)), Just(@2(xv400, xv401)), app(app(ty_@2, app(ty_Maybe, bbe)), bba)) → new_esEs1(xv300, xv400, bbe)
new_esEs(:(xv300, xv301), :(xv400, xv401), app(ty_[], ba)) → new_esEs(xv300, xv400, ba)
new_esEs0(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), app(app(app(ty_@3, cf), cg), da), cd, ce) → new_esEs0(xv300, xv400, cf, cg, da)
new_esEs(:(xv300, xv301), :(xv400, xv401), app(ty_Maybe, be)) → new_esEs1(xv300, xv400, be)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: